the_es:ES, e:E. isrcv(e)  index(e)  ||sends(lnk(e);sender(e))|| 

latex

Definitions

t  T, P  Q, x:A. B(x), sender(e), s = t, Type, Prop, A & B, x:AB(x), P  Q, pred!(e;e'), left+right, x:AB(x), pred(e), first(e), A, a<b, , {x:A| B(x) }, f(a), x:A. B(x), SWellFounded(R(x;y)), Void, x:A. B(x), False, rcv-from-on(dE;dL;info;e;l;r), type List, S  T, receives(dE;dL;pred?;info;p;e;l), sends(dE;dL;pred?;info;val;p;e;l), True, rcv(l,tg), IdLnk, ecase1(e;info;i.f(i);l,e'.g(l;e')), P & Q, EOrderAxioms(E; pred?; info), isrcv(k), es_info(es), es-oaxioms(es), es-pred?(es), es-eq(es), kind(e), es_val(es), index(e), sends(l;e), sender(e), lnk(e), isrcv(e), E, ES, {i..j}, Top, link(e), kind(e), lnk(k), s ~ t, rcv?(e), b, IdLnkDeq, Id

Lemmas

es-isrcv wf, es-E wf, event system wf, isrcv wf, kind wf, index wf, rcv?-kind, IdLnk wf, false wf, true wf, length-map, receives wf, top wf, rcv-from-on wf, idlnk-deq wf, link wf, nat wf, not wf, first wf, pred wf, assert wf, rcv? wf, sender wf, Id wf